Section: Scientific Foundations

Formal Methods for General and Domain-Specific Languages

We are working on developping and applying formal methods to the definition, analysis, and transformation of languages. These languages include general ones like C, Domain-Specific ones (DSLs) such as Kermeta  [109] , Signal  [99] , and VHDL, and Domain-Specific modelling ones (DSMLs) such as xSPEM  [78] . We use rewriting techniques embodied in the K  [117] and Maude  [87] semantical frameworks, abstract interpretation techniques, techniques inspired from program transformation and compilation, and refinement techniques. We often use Model-Driven Engineering (MDE) as a lingua franca and we believe it is a useful vessel for formal methods into software engineering practice. We fruitfully collaborate with colleagues within Inria (the Triskell team at Inria Rennes-Bretagne Atlantique and the Compsys team at Inria Grenoble Rhône-Alpes), with colleagues outside Inria (David Monniaux at Verimag, Grenoble), and with foreign colleagues (the K-framework team bi-localised in Iaşi, Romania and in Urbana Champaign, USA; the university of Aleppo, Syria). We organise events (two workshops and one summer school in 2011), supervise PhD students (one started in the Fall 2001, co-supervision with the K team) and interns, participate in PhD commitees (two in 2011) and in teaching. We have obtained financial support outside Inria from the University of Lille.